Left Termination proof of /tmp/tmpdby3mr/at.pl

Left Termination of the query pattern at(f,f) w.r.t. the given Prolog program could successfully be proven:

↳ PROLOG

  ↳ PrologToPiTRSProof

at₂(X, fido₀) :- at₂(X, mary₀), near₁(X).
at₂(ta₀, mary₀).
at₂(jm₀, mary₀).
near₁(jm₀).

With regard to the inferred argument filtering the predicates were used in the following modes:
at₂: (f,f) (f,b)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

at_2_in_aa₂(X, fido_0) -> if_at_2_in_1_aa₂(X, at_2_in_ag₂(X, mary_0))
at_2_in_ag₂(X, fido_0) -> if_at_2_in_1_ag₂(X, at_2_in_ag₂(X, mary_0))
at_2_in_ag₂(ta_0, mary_0) -> at_2_out_ag₂(ta_0, mary_0)
at_2_in_ag₂(jm_0, mary_0) -> at_2_out_ag₂(jm_0, mary_0)
if_at_2_in_1_ag₂(X, at_2_out_ag₂(X, mary_0)) -> if_at_2_in_2_ag₂(X, near_1_in_g₁(X))
near_1_in_g₁(jm_0) -> near_1_out_g₁(jm_0)
if_at_2_in_2_ag₂(X, near_1_out_g₁(X)) -> at_2_out_ag₂(X, fido_0)
if_at_2_in_1_aa₂(X, at_2_out_ag₂(X, mary_0)) -> if_at_2_in_2_aa₂(X, near_1_in_g₁(X))
if_at_2_in_2_aa₂(X, near_1_out_g₁(X)) -> at_2_out_aa₂(X, fido_0)
at_2_in_aa₂(ta_0, mary_0) -> at_2_out_aa₂(ta_0, mary_0)
at_2_in_aa₂(jm_0, mary_0) -> at_2_out_aa₂(jm_0, mary_0)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

at_2_in_aa₂(X, fido_0) -> if_at_2_in_1_aa₂(X, at_2_in_ag₂(X, mary_0))
at_2_in_ag₂(X, fido_0) -> if_at_2_in_1_ag₂(X, at_2_in_ag₂(X, mary_0))
at_2_in_ag₂(ta_0, mary_0) -> at_2_out_ag₂(ta_0, mary_0)
at_2_in_ag₂(jm_0, mary_0) -> at_2_out_ag₂(jm_0, mary_0)
if_at_2_in_1_ag₂(X, at_2_out_ag₂(X, mary_0)) -> if_at_2_in_2_ag₂(X, near_1_in_g₁(X))
near_1_in_g₁(jm_0) -> near_1_out_g₁(jm_0)
if_at_2_in_2_ag₂(X, near_1_out_g₁(X)) -> at_2_out_ag₂(X, fido_0)
if_at_2_in_1_aa₂(X, at_2_out_ag₂(X, mary_0)) -> if_at_2_in_2_aa₂(X, near_1_in_g₁(X))
if_at_2_in_2_aa₂(X, near_1_out_g₁(X)) -> at_2_out_aa₂(X, fido_0)
at_2_in_aa₂(ta_0, mary_0) -> at_2_out_aa₂(ta_0, mary_0)
at_2_in_aa₂(jm_0, mary_0) -> at_2_out_aa₂(jm_0, mary_0)

AT_2_IN_AA₂(X, fido_0) -> IF_AT_2_IN_1_AA₂(X, at_2_in_ag₂(X, mary_0))
AT_2_IN_AA₂(X, fido_0) -> AT_2_IN_AG₂(X, mary_0)
AT_2_IN_AG₂(X, fido_0) -> IF_AT_2_IN_1_AG₂(X, at_2_in_ag₂(X, mary_0))
AT_2_IN_AG₂(X, fido_0) -> AT_2_IN_AG₂(X, mary_0)
IF_AT_2_IN_1_AG₂(X, at_2_out_ag₂(X, mary_0)) -> IF_AT_2_IN_2_AG₂(X, near_1_in_g₁(X))
IF_AT_2_IN_1_AG₂(X, at_2_out_ag₂(X, mary_0)) -> NEAR_1_IN_G₁(X)
IF_AT_2_IN_1_AA₂(X, at_2_out_ag₂(X, mary_0)) -> IF_AT_2_IN_2_AA₂(X, near_1_in_g₁(X))
IF_AT_2_IN_1_AA₂(X, at_2_out_ag₂(X, mary_0)) -> NEAR_1_IN_G₁(X)

The TRS R consists of the following rules:

at_2_in_aa₂(X, fido_0) -> if_at_2_in_1_aa₂(X, at_2_in_ag₂(X, mary_0))
at_2_in_ag₂(X, fido_0) -> if_at_2_in_1_ag₂(X, at_2_in_ag₂(X, mary_0))
at_2_in_ag₂(ta_0, mary_0) -> at_2_out_ag₂(ta_0, mary_0)
at_2_in_ag₂(jm_0, mary_0) -> at_2_out_ag₂(jm_0, mary_0)
if_at_2_in_1_ag₂(X, at_2_out_ag₂(X, mary_0)) -> if_at_2_in_2_ag₂(X, near_1_in_g₁(X))
near_1_in_g₁(jm_0) -> near_1_out_g₁(jm_0)
if_at_2_in_2_ag₂(X, near_1_out_g₁(X)) -> at_2_out_ag₂(X, fido_0)
if_at_2_in_1_aa₂(X, at_2_out_ag₂(X, mary_0)) -> if_at_2_in_2_aa₂(X, near_1_in_g₁(X))
if_at_2_in_2_aa₂(X, near_1_out_g₁(X)) -> at_2_out_aa₂(X, fido_0)
at_2_in_aa₂(ta_0, mary_0) -> at_2_out_aa₂(ta_0, mary_0)
at_2_in_aa₂(jm_0, mary_0) -> at_2_out_aa₂(jm_0, mary_0)

The argument filtering Pi contains the following mapping:
at_2_in_aa₂(x1, x2) = at_2_in_aa
fido_0 = fido_0
mary_0 = mary_0
ta_0 = ta_0
jm_0 = jm_0
if_at_2_in_1_aa₂(x1, x2) = if_at_2_in_1_aa₁(x2)
at_2_in_ag₂(x1, x2) = at_2_in_ag₁(x2)
if_at_2_in_1_ag₂(x1, x2) = if_at_2_in_1_ag₁(x2)
at_2_out_ag₂(x1, x2) = at_2_out_ag₁(x1)
if_at_2_in_2_ag₂(x1, x2) = if_at_2_in_2_ag₂(x1, x2)
near_1_in_g₁(x1) = near_1_in_g₁(x1)
near_1_out_g₁(x1) = near_1_out_g
if_at_2_in_2_aa₂(x1, x2) = if_at_2_in_2_aa₂(x1, x2)
at_2_out_aa₂(x1, x2) = at_2_out_aa₂(x1, x2)
AT_2_IN_AA₂(x1, x2) = AT_2_IN_AA
IF_AT_2_IN_2_AA₂(x1, x2) = IF_AT_2_IN_2_AA₂(x1, x2)
NEAR_1_IN_G₁(x1) = NEAR_1_IN_G₁(x1)
IF_AT_2_IN_2_AG₂(x1, x2) = IF_AT_2_IN_2_AG₂(x1, x2)
IF_AT_2_IN_1_AA₂(x1, x2) = IF_AT_2_IN_1_AA₁(x2)
IF_AT_2_IN_1_AG₂(x1, x2) = IF_AT_2_IN_1_AG₁(x2)
AT_2_IN_AG₂(x1, x2) = AT_2_IN_AG₁(x2)

We have to consider all (P,R,Pi)-chains

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

AT_2_IN_AA₂(X, fido_0) -> IF_AT_2_IN_1_AA₂(X, at_2_in_ag₂(X, mary_0))
AT_2_IN_AA₂(X, fido_0) -> AT_2_IN_AG₂(X, mary_0)
AT_2_IN_AG₂(X, fido_0) -> IF_AT_2_IN_1_AG₂(X, at_2_in_ag₂(X, mary_0))
AT_2_IN_AG₂(X, fido_0) -> AT_2_IN_AG₂(X, mary_0)
IF_AT_2_IN_1_AG₂(X, at_2_out_ag₂(X, mary_0)) -> IF_AT_2_IN_2_AG₂(X, near_1_in_g₁(X))
IF_AT_2_IN_1_AG₂(X, at_2_out_ag₂(X, mary_0)) -> NEAR_1_IN_G₁(X)
IF_AT_2_IN_1_AA₂(X, at_2_out_ag₂(X, mary_0)) -> IF_AT_2_IN_2_AA₂(X, near_1_in_g₁(X))
IF_AT_2_IN_1_AA₂(X, at_2_out_ag₂(X, mary_0)) -> NEAR_1_IN_G₁(X)

The TRS R consists of the following rules:

at_2_in_aa₂(X, fido_0) -> if_at_2_in_1_aa₂(X, at_2_in_ag₂(X, mary_0))
at_2_in_ag₂(X, fido_0) -> if_at_2_in_1_ag₂(X, at_2_in_ag₂(X, mary_0))
at_2_in_ag₂(ta_0, mary_0) -> at_2_out_ag₂(ta_0, mary_0)
at_2_in_ag₂(jm_0, mary_0) -> at_2_out_ag₂(jm_0, mary_0)
if_at_2_in_1_ag₂(X, at_2_out_ag₂(X, mary_0)) -> if_at_2_in_2_ag₂(X, near_1_in_g₁(X))
near_1_in_g₁(jm_0) -> near_1_out_g₁(jm_0)
if_at_2_in_2_ag₂(X, near_1_out_g₁(X)) -> at_2_out_ag₂(X, fido_0)
if_at_2_in_1_aa₂(X, at_2_out_ag₂(X, mary_0)) -> if_at_2_in_2_aa₂(X, near_1_in_g₁(X))
if_at_2_in_2_aa₂(X, near_1_out_g₁(X)) -> at_2_out_aa₂(X, fido_0)
at_2_in_aa₂(ta_0, mary_0) -> at_2_out_aa₂(ta_0, mary_0)
at_2_in_aa₂(jm_0, mary_0) -> at_2_out_aa₂(jm_0, mary_0)